the_w:World, e:E.
FairFifo  (isrcv(kind(e)))  (t:{0..time(e)}. (match(lnk(kind(e));t;time(e)))) 

latex

Definitions

x:A. B(x), P  Q, t  T, isrcv(l;a), kind(e), loc(e), time(e), t.1, t.2, act(e), b, p  q, b, , T, True, tt, if b then t else f fi , ff, queue(l;t), Top, S  T, , match(l;t;t'), SQType(T), {T}, FairFifo, P & Q, A c B, E, A, SqStable(P), , Unit, P  Q, False, P  Q, hd(l), A  B,

Lemmas

assert wf, isrcv wf, w-ekind wf, fair-fifo wf, w-E wf, world wf, sq stable from decidable, band wf, bnot wf, w-isnull wf, w-a wf, w-kind wf, eq lnk wf, lnk wf, decidable assert, bool wf, eqtt to assert, iff transitivity, not wf, eqff to assert, assert of bnot, assert-eq-lnk, w-loc wf, w-time wf, length wf nat, w-rcvs wf, top wf, w-action wf, nat wf, w-snds wf, w-Msg wf, nth tl decomp, w-msg wf, le wf, IdLnk wf